/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30



␈↓ ↓H␈↓α␈↓ ¬MDerived Functions

␈↓ ↓H␈↓␈↓ α_A␈α⊂derived␈α⊂function␈α⊂␈↓↓f'␈↓␈α⊂of␈α⊂␈↓↓f␈↓␈α⊂contains␈α⊂a␈α⊂computation␈α⊂sequence␈α⊂of␈α⊂␈↓↓f␈↓␈α⊂in␈α⊂its␈α⊃arguments␈α⊂and
␈↓ ↓H␈↓values.␈α We␈αspeculate␈αthat␈αproving␈αassertions␈α
about␈αderived␈αfunctions␈αmay␈αbe␈αeasier␈αbecause␈α
more
␈↓ ↓H␈↓information␈α
is␈αkept.␈α
 Induction␈αon␈α
a␈αderived␈α
function␈αmay␈α
sometimes␈αcorrespond␈α
to␈αsomething␈α
like
␈↓ ↓H␈↓course-of-values␈α
induction␈α
on␈αthe␈α
original.␈α
 We␈αwould␈α
like␈α
to␈αsay␈α
"the␈α
derived␈α
function"␈αinstead
␈↓ ↓H␈↓of␈α"a␈αderived␈αfunction"␈αand␈α"the␈αcomputation␈αsequence"␈αinstead␈αof␈α"a␈αcomputation␈αsequence",␈αbut
␈↓ ↓H␈↓a␈α
single␈α
preferred␈α
notion␈α
has␈αnot␈α
yet␈α
become␈α
apparent.␈α
 Note␈αalso␈α
that␈α
the␈α
derived␈α
function␈αwill
␈↓ ↓H␈↓depend on the way the function is described and not just on the argument-value pairing.

␈↓ ↓H␈↓␈↓ α_Derived␈α_functions␈α↔are␈α_presumably␈α↔related␈α_to␈α↔their␈α_originals␈α↔by␈α_something␈α_like␈α↔the
␈↓ ↓H␈↓homomorphism␈α⊃theorem␈α⊃and␈α⊃are␈α⊃therefore␈α⊃equi-convergent.␈α⊃ [The␈α⊃homomorphism␈α⊃theorem␈α⊃is
␈↓ ↓H␈↓␈↓↓∀ff'. [(␈↓	f␈↓↓ ␈↓πo␈↓↓ f = f' ␈↓πo␈↓↓ ␈↓	y␈↓↓) ⊃ (␈↓	f␈↓↓ ␈↓πo␈↓↓ F(f) = F'(f') ␈↓πo␈↓↓ ␈↓	y␈↓↓)] ⊃ (␈↓	f␈↓↓ ␈↓πo␈↓↓ Y(F) = Y(F') ␈↓πo␈↓↓ ␈↓	y␈↓↓)]␈↓.

␈↓ ↓H␈↓␈↓ α_Here are some examples of functions and derived functions:

␈↓ ↓H␈↓␈↓ α_1.      ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x

␈↓ ↓H␈↓↓␈↓ α_f' u ← ␈↓αif␈↓↓ p ␈↓αa␈↓↓ u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ f'(h ␈↓αa␈↓↓ u . u)

␈↓ ↓H␈↓↓␈↓ α_f''(x,u) ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ f''(h x, x . u)

␈↓ ↓H␈↓↓␈↓ α_2.      f x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ f f (x + 11)

␈↓ ↓H␈↓↓␈↓ α_f'(x,v) ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ (x - 10) . v ␈↓αelse␈↓↓ [λ w . f'(␈↓αa␈↓↓ w, w)][f'(x + 11,␈↓π ␈↓↓(x␈↓π ␈↓↓+␈↓π ␈↓↓11)␈↓π ␈↓↓.␈↓π ␈↓↓v)]

␈↓ ↓H␈↓↓␈↓ α_3.      flat[x,u] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x . u ␈↓αelse␈↓↓ flat[␈↓αa␈↓↓ x, flat[␈↓αd␈↓↓ x, u]]

␈↓ ↓H␈↓↓␈↓ α_flat'[x,u,v] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ [x . u] . v ␈↓αelse␈↓↓
␈↓ ↓H␈↓↓␈↓ α_             [λ z . flat'[␈↓αa␈↓↓ x, ␈↓αa␈↓↓ z, ␈↓αa␈↓↓ x . dz]] [flat'[␈↓αd␈↓↓ x, u, ␈↓αd␈↓↓ x . v]]

␈↓ ↓H␈↓↓␈↓ α_flat''[x,u,v] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ (x . u) . v ␈↓αelse␈↓↓
␈↓ ↓H␈↓↓␈↓ α_              [λ z flat''[␈↓αa␈↓↓ x, ␈↓αa␈↓↓ z, <␈↓αa␈↓↓ x ␈↓αa␈↓↓ z> . ␈↓αd␈↓↓ z]] [flat''[␈↓αd␈↓↓ x, u, <␈↓αd␈↓↓ x u> . v]]

␈↓ ↓H␈↓↓␈↓ α_4.      flatten x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ flatten ␈↓αa␈↓↓ x * flatten ␈↓αd␈↓↓ x

␈↓ ↓H␈↓↓␈↓ α_flatten'[x,v] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> . v ␈↓αelse␈↓↓
␈↓ ↓H␈↓↓␈↓ α_                {flatten'[␈↓αa␈↓↓ x, ␈↓αa␈↓↓ x . v]} [λ z . {flatten'[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ x . ␈↓αd␈↓↓ z]} [λ w [␈↓αa␈↓↓ z * q w] . ␈↓αd␈↓↓ w]